\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $l$:IdLnk, ${\it tg}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;source($l$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($\uparrow$kind($e$) $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ ((valtype($e$) $\subseteq$r (${\it conds}$(kind($e$)).1)) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\-\\[0ex]$\Rightarrow$ \=($\forall$$p$:(\=$\forall$$e$:E.\+\+
\\[0ex]Dec(($\uparrow$isrcv($e$))
\\[0ex]\& lnk($e$) = $l$
\\[0ex]\& loc(sender($e$)) = source($l$) $\in$ Id
\\[0ex]\& ($\uparrow$kind(sender($e$)) $\in$ dom(${\it conds}$)))).
\-\\[0ex]($\forall$$k$:Knd.
\\[0ex]($\uparrow$$k$ $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ \=$k$(v:${\it conds}$($k$).1) sends on $l$ [${\it tg}$:$A$, $\lambda$$p$.let $s$,$v$ = $p$\+
\\[0ex]in
\\[0ex](${\it conds}$($k$).2)($s$,$v$) $<$state, v$>$]?[])
\-\\[0ex]$\Rightarrow$ glues(\=${\it es}$;\+
\\[0ex]$A$;
\\[0ex]($\lambda$$e$.sender($e$));
\\[0ex]($\lambda$$e$.outl((${\it conds}$(kind($e$)).2)((state when $e$),val($e$))));
\\[0ex]es{-}triggers(${\it es}$;source($l$);${\it ds}$;${\it conds}$);
\\[0ex](es{-}in{-}port(${\it es}$;$l$;${\it tg}$)$\mid$$p$)))
\-\-
\end{tabbing}